дедукции теорема

        ДЕДУКЦИИ ТЕОРЕМА (от лат. deductio — выведение) — утверждение о свойствах логической теории. Д. т. гласит: «Если имеется вывод Г, А (- В, то имеется также и вывод Г J- А —> В, где —> — знак импликации, Г — произвольное (возможно пустое) множество формул языка теории, А, В — произвольные формулы языка теории». Название «Д. т .» принадлежит Д. Гильберту и П. Бернайсу Hubert D., Bernays P. Grundlagen der Mathematik. Berlin, 1934), однако доказательство теоремы встречается еще раньше в работе Эрбрана (Herbrand /. Recherches sur la theorie de la demonstration // Travaux de la Societe des Sciences et des Letters de Varsovie. Classe III. Sciences Mathematiques et Physiques. № 33. 1930).

        Д. т. позволяет использовать при построении выводов и доказательств вспомогательное правило: «Если необходимо вывести или доказать импликативную формулу, то достаточно осуществить вспомогательный вывод, в котором в качестве дополнительного допущения принимается антецедент этой формулы, а обосновывается ее консеквент». Обычно такой дополнительный вывод построить значительно проще.

        Доказательство Д. т. осуществляется методом возвратной математической индукции. Цель доказательства — показать, как вспомогательный вывод Г, А |- В может быть на каждом шаге вывода перестроен в вывод Г \-А —> В. При этом стандартное доказательство основывается на использовании следующих дедуктивных принципов: «утверждение консеквента» А — > ( В — > А ) и «самодистрибутивность импликации» ( А — > ( В — > А)) — > ( А —» В) —> (А - С), а также «закон тождества» А —> А, получаемый из этих аксиом. Поскольку указанные формулы включаются в аксиоматику интуиционистской логики, доказательство Д. т. для этой логической теории и более сильных (включая классическую логику) является стандартным. Однако далеко не во всех логических теориях принимаются эти дедуктивные принципы. В ряде исчислений неклассической логики доказательство соответствующей формы Д. т. оказывается нетривиальной процедурой. Для некоторых теорий, напр. для отвергающих импликативную формулировку закона тождества, Д. т. доказать невозможно.

        Д.В. Зайцев